Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    from(X)  → cons(X,n__from(s(X)))
2:    2ndspos(0,Z)  → rnil
3:    2ndspos(s(N),cons(X,Z))  → 2ndspos(s(N),cons2(X,activate(Z)))
4:    2ndspos(s(N),cons2(X,cons(Y,Z)))  → rcons(posrecip(Y),2ndsneg(N,activate(Z)))
5:    2ndsneg(0,Z)  → rnil
6:    2ndsneg(s(N),cons(X,Z))  → 2ndsneg(s(N),cons2(X,activate(Z)))
7:    2ndsneg(s(N),cons2(X,cons(Y,Z)))  → rcons(negrecip(Y),2ndspos(N,activate(Z)))
8:    pi(X)  → 2ndspos(X,from(0))
9:    plus(0,Y)  → Y
10:    plus(s(X),Y)  → s(plus(X,Y))
11:    times(0,Y)  → 0
12:    times(s(X),Y)  → plus(Y,times(X,Y))
13:    square(X)  → times(X,X)
14:    from(X)  → n__from(X)
15:    activate(n__from(X))  → from(X)
16:    activate(X)  → X
There are 15 dependency pairs:
17:    2ndspos#(s(N),cons(X,Z))  → 2ndspos#(s(N),cons2(X,activate(Z)))
18:    2ndspos#(s(N),cons(X,Z))  → ACTIVATE(Z)
19:    2ndspos#(s(N),cons2(X,cons(Y,Z)))  → 2ndsneg#(N,activate(Z))
20:    2ndspos#(s(N),cons2(X,cons(Y,Z)))  → ACTIVATE(Z)
21:    2ndsneg#(s(N),cons(X,Z))  → 2ndsneg#(s(N),cons2(X,activate(Z)))
22:    2ndsneg#(s(N),cons(X,Z))  → ACTIVATE(Z)
23:    2ndsneg#(s(N),cons2(X,cons(Y,Z)))  → 2ndspos#(N,activate(Z))
24:    2ndsneg#(s(N),cons2(X,cons(Y,Z)))  → ACTIVATE(Z)
25:    PI(X)  → 2ndspos#(X,from(0))
26:    PI(X)  → FROM(0)
27:    PLUS(s(X),Y)  → PLUS(X,Y)
28:    TIMES(s(X),Y)  → PLUS(Y,times(X,Y))
29:    TIMES(s(X),Y)  → TIMES(X,Y)
30:    SQUARE(X)  → TIMES(X,X)
31:    ACTIVATE(n__from(X))  → FROM(X)
The approximated dependency graph contains 3 SCCs: {27}, {29} and {17,19,21,23}. Hence the TRS is terminating.
Tyrolean Termination Tool  (2.28 seconds)   ---  May 3, 2006